1  /-
  2  Copyright (c) 2019 Amelia Livingston. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Amelia Livingston
  5  -/
  6  
  7  import group_theory.congruence
src         └─────────────────────┘
  8  import algebra.associated
src         └────────────────┘
  9  import tactic.abel
src         └─────────┘
 10  
 11  /-
 12  
 13  # Localizations of commutative monoids
 14  
 15  The standard congruence relation (an equivalence relation preserving a binary operation) used to
 16  define commutative ring localizations does not rely on the ring's addition. For a commutative
 17  monoid `X` and submonoid `Y`, this relation can be expressed as
 18  `∀ (x₁, y₁) (x₂, y₂) : X × Y, x ∼ y ↔ ∃ c ∈ Y, c * x₁ * y₂ = c * x₂ * y₁`, or, equivalently, as the
 19  unique congruence relation `r` on `X × Y` such that for any other congruence relation `r'` on
 20  `X × Y` where for all `y ∈ Y`, `(1, 1) ∼ (y, y)` under `r'`, we have that `(x₁, y₁) ∼ (x₂, y₂)` by
 21  `r'` implies `(x₁, y₁) ∼ (x₂, y₂)` by `r`.
 22  
 23  The first half of the file contains basic lemmas about the localization of `X` at `Y` - the
 24  commutative monoid we get when we quotient `X × Y` by this congruence relation - and some
 25  associated monoid homomorphisms: the quotient map, `localization.mk`, the quotient map restricted
 26  to `X × {1}`, `localization.monoid.of`, and the quotient map restricted to `Y × {1}`,
 27  `localization.monoid.to_units`, whose image is contained in the unit group of the localization of
 28  `X` at `Y`.
 29  Subsequently we prove basic lemmas about `localization.monoid.lift'` (constructive version) and
 30  `localization.monoid.lift` (classical version): given a `comm_monoid` homomorphism `f : X → Z`
 31  mapping elements of a submonoid `Y` to invertible elements of `Z`, these are the homomorphism
 32  from the localization of `X` at `Y` sending `⟦(x, y)⟧` to `f(x) * f(y)⁻¹`. If `f(Y)` is contained
 33  in a submonoid `W` of `Z`, we can also define the map from the localization of `X` at `Y`
 34  to the localization of `Z` at `W` induced by `(of W) ∘ f`, where `of W` is the natural map from `Z`
 35  to the localization of `Z` at `W`. This is called `localization.monoid.map`.
 36  
 37  ## Implementation notes
 38  
 39  The infimum form of the localization congruence relation is chosen as 'canonical' here, since it
 40  shortens many proofs.
 41  
 42  The `private def` `r'.rel` and the lemmas `r'.add, r'.transitive` are to enable the use of the
 43  `abel` tactic for both the additive and multiplicative proofs that the 'usual' localization
 44  congruence relation is a congruence relation.
 45  
 46  There is only a multiplicative version for any lemma or definition relying on a unit group of a
 47  `comm_monoid`; additive versions would require additive unit groups.
 48  
 49  ## Tags
 50  localization, monoid localization, quotient monoid, congruence relation
 51  
 52  -/
 53  variables {X : Type*}
 54  
 55  namespace submonoid
 56  
 57  /-- The congruence relation on `X × Y`, `X` a `comm_monoid` and `Y` a submonoid of `X`, whose
 58      quotient is the localization of `X` at `Y`, defined as the unique congruence relation on
 59      `X × Y` such that for any other congruence relation `s` on `X × Y` where for all `y ∈ Y`,
 60      `(1, 1) ∼ (y, y)` under `s`, we have that `(x₁, y₁) ∼ (x₂, y₂)` by `s` implies
 61      `(x₁, y₁) ∼ (x₂, y₂)` by `r`. -/
 62  @[to_additive "The congruence relation on `X × Y`, `X` an `add_comm_monoid` and `Y` an `add_submonoid` of `X`, whose quotient is the localization of `X` at `Y`, defined as the unique congruence relation on `X × Y` such that for any other congruence relation `s` on `X × Y` where for all `y ∈ Y`, `(0, 0) ∼ (y, y)` under `s`, we have that `(x₁, y₁) ∼ (x₂, y₂)` by `s` implies `(x₁, y₁) ∼ (x₂, y₂)` by `r`."]
doc    └─────────┘
 63  def r [comm_monoid X] (Y : submonoid X) : con (X × Y) :=
id          └─────────┘        └───────┘     └─┘    
src         └─────────┘         └───────┘      └─┘    
typ         └─────────┘        └───────┘     └─┘    
doc                             └───────┘      └─┘
 64  lattice.Inf {c | ∀ y : Y, c 1 (y, y)}
id   └─────────┘                 
src  └─────────┘                  
typ  └─────────┘                 
doc  └─────────┘
 65  
 66  end submonoid
 67  
 68  namespace add_submonoid
 69  
 70  variables [add_comm_monoid X]
id              └─────────────┘
src             └─────────────┘
typ             └─────────────┘
 71  
 72  /-- An alternate form of the `add_monoid` localization relation, stated here for readability of the
 73      next few lemmas. -/
 74  private def r'.rel (Y : add_submonoid X) (a b : X × Y) :=
id                           └───────────┘            
src                          └───────────┘             
typ                          └───────────┘            
doc                          └───────────┘
 75  ∃ c : Y, (c : X) + (a.1 + b.2) = c + (b.1 + a.2)
id                              
src                                     
typ                             
 76  
 77  lemma r'.transitive {Y : add_submonoid X} : transitive (r'.rel Y) :=
id                            └───────────┘     └────────┘  └────┘ 
src                           └───────────┘      └────────┘  └────┘
typ                           └───────────┘     └────────┘  └────┘ 
doc                           └───────────┘                  └────┘
 78  λ a b c ⟨m, hm⟩ ⟨n, hn⟩, ⟨n + m + b.2,
id                            
src                                   
typ                           
 79    calc
 80      ↑n + ↑m + ↑b.2 + (a.1 + ↑c.2)
id                    
src                      
typ                   
 81        = ↑n + (↑m + (b.1 + ↑a.2)) + ↑c.2 : by rw ←hm; abel
id                                      └┘
src                                    └──┘    └────
typ                                 └──┘└┘  └────
doc                                               └──┘    └────
txt                                               └──┘    └────
par                                               └──┘    └────
pid                                                 └┘        
st                                               └─────────────
 82    ... = ↑m + (↑n + (c.1 + ↑b.2)) + ↑a.2 : by rw ←hn; abel
id                                      └┘
src  ─┘                                └──┘    └────
typ  ─┘                             └──┘└┘  └────
doc  ─┘                                           └──┘    └────
txt  ─┘                                           └──┘    └────
par  ─┘                                           └──┘    └────
pid  ─┘                                             └┘        
st   ─┘                                          └─────────────
 83    ... = ↑n + ↑m + ↑b.2 + (c.1 + ↑a.2) : by abel⟩
id                        
src  ─┘                              └──┘
typ  ─┘                           └──┘
doc  ─┘                                         └──┘
txt  ─┘                                         └──┘
par  ─┘                                         └──┘
pid  ─┘
st   ─┘                                        └───┘
 84  
 85  lemma r'.add {Y : add_submonoid X} {a b c d} :
id                     └───────────┘ 
src                    └───────────┘
typ                    └───────────┘ 
doc                    └───────────┘
 86    r'.rel Y a b → r'.rel Y c d → r'.rel Y (a + c) (b + d) :=
id     └────┘      └────┘      └────┘          
src    └────┘         └────┘         └────┘             
typ    └────┘      └────┘      └────┘          
doc    └────┘         └────┘         └────┘
 87  λ ⟨m, hm⟩ ⟨n, hn⟩, ⟨m + n,
id                     
src                        
typ                    
 88    calc
 89      ↑m + ↑n + (a.1 + c.1 + (↑b.2 + ↑d.2))
id                        
src                           
typ                       
 90        = ↑n + c.1 + (↑m + (b.1 + ↑a.2)) + ↑d.2 : by rw ←hm; abel
id                                         └┘
src                                        └──┘    └────
typ                                    └──┘└┘  └────
doc                                                     └──┘    └────
txt                                                     └──┘    └────
par                                                     └──┘    └────
pid                                                       └┘        
st                                                     └─────────────
 91    ... = (↑m + (b.1 + ↑a.2)) + (↑n + (d.1 + ↑c.2)) : by rw ←hn; abel
id                                             └┘
src  ─┘                                        └──┘    └────
typ  ─┘                                    └──┘└┘  └────
doc  ─┘                                                     └──┘    └────
txt  ─┘                                                     └──┘    └────
par  ─┘                                                     └──┘    └────
pid  ─┘                                                       └┘        
st   ─┘                                                    └─────────────
 92    ... = ↑m + ↑n + (b.1 + d.1 + (↑a.2 + ↑c.2)) : by abel⟩
id                            
src  ─┘                                    └──┘
typ  ─┘                                └──┘
doc  ─┘                                                 └──┘
txt  ─┘                                                 └──┘
par  ─┘                                                 └──┘
pid  ─┘
st   ─┘                                                └───┘
 93  
 94  /-- An alternate form of the congruence relation on `X × Y`, `X` an `add_comm_monoid` and `Y` an
 95      `add_submonoid` of `X`, whose quotient is the localization of `X` at `Y`. Its equivalence to
 96      `r` can be useful for proofs. -/
 97  def r' (Y : add_submonoid X) : add_con (X × Y) :=
id               └───────────┘     └─────┘    
src              └───────────┘      └─────┘    
typ              └───────────┘     └─────┘    
doc              └───────────┘      └─────┘
 98  { r := λ a b, ∃ c : Y, (c : X) + (a.1 + b.2) = c + (b.1 + a.2),
id                                          
src                                                   
typ                                         
 99    iseqv := ⟨λ _, ⟨0, rfl⟩, λ _ _ ⟨c, hc⟩, ⟨c, hc.symm⟩, r'.transitive⟩,
id                       └─┘         └┘         └───┘   └───────────┘
src                       └─┘                        └───┘   └───────────┘
typ                      └─┘         └┘         └───┘   └───────────┘
100    add' := λ a b c d, r'.add }
id                    └────┘
src                       └────┘
typ                   └────┘
101  
102  end add_submonoid
103  
104  variables [comm_monoid X] (Y : submonoid X) {Z : Type*} [comm_monoid Z]
id              └─────────┘         └───────┘                 └─────────┘
src             └─────────┘         └───────┘                 └─────────┘
typ             └─────────┘         └───────┘                 └─────────┘
doc                                 └───────┘
st                                  └───────┘
105  
106  namespace submonoid
107  
108  /-- An alternate form of the congruence relation on `X × Y`, `X` a `comm_monoid` and `Y` a
109      submonoid of `X`, whose quotient is the localization of `X` at `Y`. Its equivalence to `r` can
110      be useful for proofs. -/
111  def r' : con (X × Y) :=
id            └─┘    
src           └─┘    
typ           └─┘    
doc           └─┘
112  { r := λ a b, ∃ c : Y, (c : X) * (a.1 * b.2) = c * (b.1 * a.2),
id                                          
src                                                   
typ                                         
113    iseqv := ⟨λ _, ⟨1, rfl⟩, λ _ _ ⟨c, hc⟩, ⟨c, hc.symm⟩,
id                       └─┘         └┘         └───┘
src                       └─┘                        └───┘
typ                      └─┘         └┘         └───┘
114      @add_submonoid.r'.transitive (additive X) _ $ submonoid.to_add_submonoid Y⟩,
id        └─────────────────────────┘  └──────┘       └────────────────────────┘ 
src       └─────────────────────────┘  └──────┘        └────────────────────────┘
typ       └─────────────────────────┘  └──────┘       └────────────────────────┘ 
doc                                                    └────────────────────────┘
115    mul' := @add_submonoid.r'.add (additive X) _ $ submonoid.to_add_submonoid Y }
id              └──────────────────┘  └──────┘       └────────────────────────┘ 
src             └──────────────────┘  └──────┘        └────────────────────────┘
typ             └──────────────────┘  └──────┘       └────────────────────────┘ 
doc                                                   └────────────────────────┘
116  
117  attribute [to_additive add_submonoid.r'] submonoid.r'
id                                            └──────────┘
src                                           └──────────┘
typ                                           └──────────┘
doc             └─────────┘                   └──────────┘
118  
119  /-- The congruence relation used to localize a `comm_monoid` at a submonoid can be expressed
120      equivalently as an infimum (see `submonoid.r`) or explicitly (see `submonoid.r'`). -/
121  @[to_additive "The additive congruence relation used to localize an `add_comm_monoid` at a submonoid can be expressed equivalently as an infimum (see `add_submonoid.r`) or explicitly (see `add_submonoid.r'`)."]
doc    └─────────┘
122  theorem r_eq_r' : Y.r = Y.r' :=
id                     └┘  └─┘
src                     └┘   └─┘
typ                    └┘  └─┘
doc                     └┘    └─┘
123  le_antisymm (lattice.Inf_le $ λ _, ⟨1, by norm_num⟩) $
id   └─────────┘  └────────────┘     
src  └─────────┘  └────────────┘               └──────┘
typ  └─────────┘  └────────────┘              └──────┘
doc                                            └──────┘
txt                                            └──────┘
par                                            └──────┘
st                                            └───────┘
124    lattice.le_Inf $ λ b H x y ⟨t, ht⟩,
id     └────────────┘         
src    └────────────┘
typ    └────────────┘         
125      begin
st       └─────
126        rw [show x = (1 * x.1, 1 * x.2), by simp, show y = (1 * y.1, 1 * y.2), by simp],
id                                                                    
src        └──┘     └┘ └────┘  └──────┘└──┘└┘      └┘  └────┘  └──────┘└──┘
typ        └──┘     └┘ └────┘ └──────┘└──┘└┘     └┘  └────┘ └──────┘└──┘
doc        └──┘       └┘  └────┘  └──────┘└──┘└┘       └┘  └────┘  └──────┘└──┘
txt        └──┘       └┘  └────┘  └──────┘└──┘└┘       └┘  └────┘  └──────┘└──┘
par        └──┘       └┘  └────┘  └──────┘└──┘└┘       └┘  └────┘  └──────┘└──┘
pid          └┘       └┘  └────┘  └────────────┘       └┘  └────┘  └───────────┘
st   ────────────────────────────────────────┘└───┘└───────────────────────────────┘└───┘└──
127        refine b.trans
id                └─────┘
src        └─────┘└─────┘
typ        └─────┘└─────┘
doc        └─────┘└─────┘
txt        └─────┘       
par        └─────┘       
pid                     
st   ─────────────────────
128         (show b _ ((t : X) * y.2 * x.1, t * y.2 * x.2), from
id                         
src  ──────┘      └─┘   └─┘ └┘  └─┘  └──┘   └─┘  └─────────
typ  ──────┘     └─┘   └─┘└┘  └─┘  └──┘   └─┘  └─────────
doc  ──────┘      └─┘   └─┘ └┘  └─┘  └──┘   └─┘  └─────────
txt  ──────┘      └─┘   └─┘ └┘  └─┘  └──┘   └─┘  └─────────
par  ──────┘      └─┘   └─┘ └┘  └─┘  └──┘   └─┘  └─────────
pid  ──────┘      └─┘   └─┘ └┘  └─┘  └──┘   └─┘  └─────────
st   ────────────────────────────────────────────────────────────
129           b.mul (H (t * y.2)) $ b.refl (x.1, x.2)) _,
id            └───┘              └────┘       
src  ────────┘└───┘      └───┘ └────┘  └──┘ └────┘
typ  ────────┘└───┘   └───┘ └────┘  └──┘└────┘
doc  ────────┘└───┘      └───┘ └────┘  └──┘ └────┘
txt  ────────┘           └───┘         └──┘ └────┘
par  ────────┘           └───┘         └──┘ └────┘
pid  ────────┘           └───┘         └──┘ └────┘
st   ──────────────────────────────────────────────────┘└─
130        rw [mul_assoc, mul_comm _ x.1, ht, mul_comm y.1, mul_assoc, mul_comm y.2,
id             └───────┘  └──────┘       └┘  └──────┘     └───────┘  └──────┘ 
src        └──┘└───────┘└┘└──────┘└─┘ └──┘  └┘└──────┘ └──┘└───────┘└┘└──────┘ └───
typ        └──┘└───────┘└┘└──────┘└─┘└──┘└┘└┘└──────┘└──┘└───────┘└┘└──────┘└───
doc        └──┘         └┘        └─┘ └──┘  └┘         └──┘         └┘         └───
txt        └──┘         └┘        └─┘ └──┘  └┘         └──┘         └┘         └───
par        └──┘         └┘        └─┘ └──┘  └┘         └──┘         └┘         └───
pid          └┘         └┘        └─┘ └──┘  └┘         └──┘         └┘         └───
st   ──────────────────┘└────────────┘└────┘└──────────┘└───────────┘└──────────┘└───
131            ←mul_assoc, ←mul_assoc],
id              └───────┘   └───────┘
src  ──────────┘└───────┘└─┘└───────┘
typ  ──────────┘└───────┘└─┘└───────┘
doc  ──────────┘         └─┘         
txt  ──────────┘         └─┘         
par  ──────────┘         └─┘         
pid  ──────────┘         └─┘         
st   ───────────────────┘└──────────┘└──
132        exact b.mul (b.symm $ H $ t * x.2) (b.refl (y.1, y.2))
id               └───┘  └────┘              └────┘       
src        └────┘└───┘ └────┘      └──┘ └────┘  └──┘ └────
typ        └────┘└───┘ └────┘   └──┘ └────┘  └──┘└────
doc        └────┘└───┘ └────┘      └──┘ └────┘  └──┘ └────
txt        └────┘                  └──┘         └──┘ └────
par        └────┘                  └──┘         └──┘ └────
pid                               └──┘         └──┘ └──┘
st   ─────────────────────────────────────────────────────────────
133      end
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
134  
135  end submonoid
136  
137  variables (X)
138  
139  /-- The localization of a `comm_monoid` at one of its submonoids. -/
140  @[to_additive add_monoid_localization "The localization of an `add_comm_monoid` at one of its submonoids."]
doc    └─────────┘
141  def monoid_localization := Y.r.quotient
id                              └┘└───────┘
src                              └┘└───────┘
typ                             └┘└───────┘
doc                              └┘└───────┘
142  
143  variables {X Y}
144  
145  namespace monoid_localization
146  
147  /-- For all `y` in `Y`, a submonoid of a `comm_monoid` `X`, `(1, 1) ∼ (y, y)` under the relation
148      defining the localization of `X` at `Y`. -/
149  @[to_additive "For all `y` in `Y`, a submonoid of an `add_comm_monoid` `X`, `(0, 0) ∼ (y, y)` under the relation defining the localization of `X` at `Y`."]
doc    └─────────┘
150  lemma one_rel (y : Y) : Y.r 1 (y, y) := by rw Y.r_eq_r'; use 1; norm_num
id                          └┘     
src                           └┘               └─┘           └───┘  └────────
typ                         └┘             └─┘└───────┘  └───┘  └────────
doc                           └┘                └─┘           └───┘  └────────
txt                                             └─┘           └───┘  └────────
par                                             └─┘           └───┘  └────────
pid                                                                       
st                                             └──────────────────────────────
151  
src  
typ  
doc  
txt  
par  
pid  
st   
152  /-- Given a `comm_monoid` `X` and submonoid `Y`, `mk` sends `x : X`, `y ∈ Y` to the equivalence
153      class of `(x, y)` in the localization of `X` at `Y`. -/
154  @[to_additive "Given an `add_comm_monoid` `X` and submonoid `Y`, `mk` sends `x : X`, `y ∈ Y` to the equivalence class of `(x, y)` in the localization of `X` at `Y`."]
doc    └─────────┘
155  def mk (x : X) (y : Y) : monoid_localization X Y := Y.r.mk' (x, y)
id                          └─────────────────┘      └┘└──┘   
src                           └─────────────────┘         └┘└──┘ 
typ                         └─────────────────┘      └┘└──┘   
doc                           └─────────────────┘         └┘└──┘
156  
157  @[elab_as_eliminator, to_additive]
doc    └────────────────┘  └─────────┘
158  theorem ind {p : monoid_localization X Y → Prop}
id                    └─────────────────┘  
src                   └─────────────────┘
typ                   └─────────────────┘  
doc                   └─────────────────┘
159    (H : ∀ (y : X × Y), p (mk y.1 y.2)) (x) : p x :=
id                        └┘              
src                          └┘     
typ                       └┘              
doc                           └┘
160  by rcases x; convert H x; exact prod.mk.eta.symm
id                                └──────────────┘
src     └─────┘   └──────┘    └────┘└──────────────┘
typ     └─────┘  └──────┘  └────┘└──────────────┘
doc     └─────┘   └──────┘    └────┘                
txt     └─────┘   └──────┘    └────┘                
par     └─────┘   └──────┘    └────┘                
pid                                              
st     └──────────────────────────────────────────────
161  
src  
typ  
doc  
txt  
par  
pid  
st   
162  @[elab_as_eliminator, to_additive]
doc    └────────────────┘  └─────────┘
163  theorem induction_on {p : monoid_localization X Y → Prop} (x)
id                             └─────────────────┘  
src                            └─────────────────┘
typ                            └─────────────────┘  
doc                            └─────────────────┘
164    (H : ∀ (y : X × Y), p (mk y.1 y.2)) : p x := ind H x
id                        └┘              └─┘  
src                          └┘                  └─┘
typ                       └┘              └─┘  
doc                           └┘
165  
166  @[to_additive] lemma exists_rep (x) : ∃ y : X × Y, mk y.1 y.2 = x :=
id                                                 └┘      
src                                                  └┘       
typ                                                └┘      
doc    └─────────┘                                      └┘
167  induction_on x $ λ y, ⟨y, rfl⟩
id   └──────────┘           └─┘
src  └──────────┘              └─┘
typ  └──────────┘           └─┘
168  
169  @[to_additive] instance : has_mul (monoid_localization X Y) := Y.r.has_mul
id                             └─────┘  └─────────────────┘       └┘└──────┘
src                            └─────┘  └─────────────────┘          └┘└──────┘
typ                            └─────┘  └─────────────────┘       └┘└──────┘
doc    └─────────┘                      └─────────────────┘          └┘└──────┘
170  
171  @[to_additive] instance : comm_monoid (monoid_localization X Y) :=
id                             └─────────┘  └─────────────────┘  
src                            └─────────┘  └─────────────────┘
typ                            └─────────┘  └─────────────────┘  
doc    └─────────┘                          └─────────────────┘
172  Y.r.comm_monoid
id   └┘└──────────┘
src   └┘└──────────┘
typ  └┘└──────────┘
doc   └┘└──────────┘
173  
174  @[to_additive] instance : inhabited (monoid_localization X Y) := ⟨1⟩
id                             └───────┘  └─────────────────┘  
src                            └───────┘  └─────────────────┘
typ                            └───────┘  └─────────────────┘  
doc    └─────────┘                        └─────────────────┘
175  
176  @[to_additive] protected lemma eq {a₁ b₁} {a₂ b₂ : Y} :
id                                                      
typ                                                     
doc    └─────────┘
177    mk a₁ a₂ = mk b₁ b₂ ↔ ∀ c : con (X × Y), (∀ y : Y, c 1 (y, y)) → c (a₁, a₂) (b₁, b₂) :=
id     └┘ └┘ └┘  └┘ └┘ └┘        └─┘                          └┘  └┘  └┘  └┘
src    └┘        └┘              └─┘                                          
typ    └┘ └┘ └┘  └┘ └┘ └┘        └─┘                          └┘  └┘  └┘  └┘
doc    └┘         └┘               └─┘
178  Y.r.eq.trans $ iff.rfl
id   └┘└─┘└────┘   └─────┘
src   └┘└─┘└────┘   └─────┘
typ  └┘└─┘└────┘   └─────┘
doc   └┘└─┘
179  
180  @[to_additive] protected lemma eq' {a₁ b₁} {a₂ b₂ : Y} :
id                                                       
typ                                                      
doc    └─────────┘
181    mk a₁ a₂ = mk b₁ b₂ ↔ ∃ c : Y, (c : X) * (a₁ * b₂) = c * (b₁ * a₂) :=
id     └┘ └┘ └┘  └┘ └┘ └┘                └┘  └┘      └┘  └┘
src    └┘        └┘                                         
typ    └┘ └┘ └┘  └┘ └┘ └┘                └┘  └┘      └┘  └┘
doc    └┘         └┘
182  ⟨λ h, let ⟨w, hw⟩ := show Y.r' (a₁, a₂) (b₁, b₂), by rw [←Y.r_eq_r', ←con.eq]; exact h in ⟨w, hw⟩,
id        └─┘    └┘          └─┘ └┘  └┘  └┘  └┘                       └────┘         
src                             └─┘                     └───┘         └─┘└────┘  └────┘ 
typ       └─┘    └┘          └─┘ └┘  └┘  └┘  └┘      └───┘└───────┘└─┘└────┘  └────┘
doc                             └─┘                       └───┘         └─┘└────┘  └────┘ 
txt                                                       └───┘         └─┘        └────┘ 
par                                                       └───┘         └─┘        └────┘ 
pid                                                         └─┘         └─┘              
st                                                       └─────────────┘└───────┘└────────┘
183   λ ⟨w, hw⟩, by erw [Y.r.eq, Y.r_eq_r']; exact ⟨w, hw⟩⟩
id                                                   └┘
src                 └───┘      └┘           └────┘  └┘  
typ                └───┘└────┘└┘└───────┘  └────┘ └┘└┘
doc                 └───┘      └┘           └────┘  └┘  
txt                 └───┘      └┘           └────┘  └┘  
par                 └───┘      └┘           └────┘  └┘  
pid                    └┘      └┘                  └┘  
st                 └──────────┘└─────────┘└─────────────┘
184  
185  @[to_additive] lemma mk_eq_of_eq {a₁ b₁} {a₂ b₂ : Y} (h : (a₂ : X) * b₁ = b₂ * a₁) :
id                                                             └┘      └┘  └┘  └┘
src                                                                             
typ                                                            └┘      └┘  └┘  └┘
doc    └─────────┘
186    mk a₁ a₂ = mk b₁ b₂ :=
id     └┘ └┘ └┘  └┘ └┘ └┘
src    └┘        └┘
typ    └┘ └┘ └┘  └┘ └┘ └┘
doc    └┘         └┘
187  monoid_localization.eq'.2 $ ⟨1, by rw [mul_comm b₁, h, mul_comm a₁]⟩
id   └─────────────────────┘               └──────┘ └┘    └──────┘ └┘
src  └─────────────────────┘           └──┘└──────┘  └┘ └┘└──────┘  
typ  └─────────────────────┘           └──┘└──────┘└┘└┘└┘└──────┘└┘
doc                                     └──┘          └┘ └┘          
txt                                     └──┘          └┘ └┘          
par                                     └──┘          └┘ └┘          
pid                                       └┘          └┘ └┘          
st                                     └──────────────┘└─┘└───────────┘
188  
189  @[simp, to_additive] lemma mk_self' (x : Y) : mk (x : X) x = 1 :=
id                                                └┘        
src                                                └┘           
typ                                               └┘        
doc    └──┘  └─────────┘                           └┘
190  monoid_localization.eq.2 $ λ c h, c.symm $ h x
id   └────────────────────┘         └───┘    
src  └────────────────────┘            └───┘
typ  └────────────────────┘         └───┘    
doc                                     └───┘
191  
192  @[simp, to_additive] lemma mk_self {x} (hx : x ∈ Y) : mk x ⟨x, hx⟩ = 1 :=
id                                                      └┘     └┘  
src                                                       └┘           
typ                                                     └┘     └┘  
doc    └──┘  └─────────┘                                   └┘
193  mk_self' ⟨x, hx⟩
id   └──────┘    └┘
src  └──────┘
typ  └──────┘    └┘
194  
195  @[simp, to_additive] lemma mk_mul_mk (x y) (s t : Y) :
id                                                     
typ                                                    
doc    └──┘  └─────────┘
196    mk x s * mk y t = mk (x * y) (s * t) := rfl
id     └┘    └┘    └┘              └─┘
src    └┘      └┘      └┘                  └─┘
typ    └┘    └┘    └┘              └─┘
doc    └┘       └┘       └┘
197  
198  /-- Definition of the function on the localization of a `comm_monoid` at a submonoid induced by a
199      function that is constant on the equivalence classes of the localization relation. -/
200  @[simp, to_additive "Definition of the function on the localization of an `add_comm_monoid` at an `add_submonoid` induced by a function that is constant on the equivalence classes of the localization relation."]
doc    └──┘  └─────────┘
201  lemma lift_on_beta {β} (f : (X × Y) → β) (H : ∀ a b, Y.r a b → f a = f b) (x y) :
id                                                  └┘         
src                                                       └┘           
typ                                                 └┘         
doc                                                        └┘
202  con.lift_on (mk x y) f H = f (x, y) := rfl
id   └─────────┘  └┘               └─┘
src  └─────────┘  └┘                      └─┘
typ  └─────────┘  └┘               └─┘
doc  └─────────┘  └┘
203  
204  /-- Natural homomorphism sending `x : X`, `X` a `comm_monoid`, to the equivalence class of
205      `(x, 1)` in the localization of `X` at a submonoid. For a `comm_ring` localization, this is
206      a ring homomorphism named `localization.of`. -/
207  @[to_additive "Natural homomorphism sending `x : X`, `X` an `add_comm_monoid`, to the equivalence class of `(x, 0)` in the localization of `X` at a submonoid."]
doc    └─────────┘
208  def of (Y) : X →* monoid_localization X Y :=
id                 └┘ └─────────────────┘  
src                 └┘ └─────────────────┘
typ                └┘ └─────────────────┘  
doc                 └┘ └─────────────────┘
209  Y.r.mk'.comp ⟨λ x, (x, 1), refl 1, λ _ _, by simp only [prod.mk_mul_mk, one_mul]⟩
id   └┘└──┘└───┘            └──┘                       └────────────┘  └─────┘
src   └┘└──┘└───┘              └──┘              └─────────┘└────────────┘└┘└─────┘
typ  └┘└──┘└───┘            └──┘            └─────────┘└────────────┘└┘└─────┘
doc   └┘└──┘└───┘                                 └─────────┘              └┘       
txt                                               └─────────┘              └┘       
par                                               └─────────┘              └┘       
pid                                                   └──┘└┘              └┘       
st                                               └──────────────────────────────────┘
210  
211  @[to_additive] lemma of_ker_iff {x y} : con.ker (of Y) x y ↔ Y.r (x, 1) (y, 1) :=
id                                           └─────┘  └┘      └┘      
src                                          └─────┘  └┘          └┘       
typ                                          └─────┘  └┘      └┘      
doc    └─────────┘                           └─────┘  └┘           └┘
212  con.eq _
id   └────┘
src  └────┘
typ  └────┘
doc  └────┘
213  
214  @[to_additive] lemma of_eq_mk (x) : of Y x = mk x 1 := rfl
id                                       └┘    └┘       └─┘
src                                      └┘      └┘        └─┘
typ                                      └┘    └┘       └─┘
doc    └─────────┘                       └┘       └┘
215  
216  @[simp, to_additive] lemma of_mul_mk (x y v) : of Y x * mk y v = mk (x * y) v :=
id                                                  └┘    └┘    └┘      
src                                                 └┘      └┘      └┘    
typ                                                 └┘    └┘    └┘      
doc    └──┘  └─────────┘                            └┘       └┘       └┘
217  by rw [of_eq_mk, mk_mul_mk, one_mul]
id          └──────┘  └───────┘  └─────┘
src     └──┘└──────┘└┘└───────┘└┘└─────┘└─
typ     └──┘└──────┘└┘└───────┘└┘└─────┘└─
doc     └──┘        └┘         └┘       └─
txt     └──┘        └┘         └┘       └─
par     └──┘        └┘         └┘       └─
pid       └┘        └┘         └┘       
st     └───────────┘└─────────┘└───────┘
218  
src  
typ  
doc  
txt  
par  
pid  
st   
219  @[to_additive] lemma mk_eq_mul_mk_one (x y) : mk x y = of Y x * mk 1 y :=
id                                                 └┘    └┘    └┘   
src                                                └┘      └┘      └┘
typ                                                └┘    └┘    └┘   
doc    └─────────┘                                 └┘       └┘       └┘
220  by rw [of_mul_mk, mul_one]
id          └───────┘  └─────┘
src     └──┘└───────┘└┘└─────┘└─
typ     └──┘└───────┘└┘└─────┘└─
doc     └──┘         └┘       └─
txt     └──┘         └┘       └─
par     └──┘         └┘       └─
pid       └┘         └┘       
st     └────────────┘└───────┘
221  
src  
typ  
doc  
txt  
par  
pid  
st   
222  @[simp, to_additive] lemma mk_mul_cancel_right (x : X) (y : Y) :
id                                                              
typ                                                             
doc    └──┘  └─────────┘
223    mk (x * y) y = of Y x :=
id     └┘        └┘  
src    └┘           └┘
typ    └┘        └┘  
doc    └┘             └┘
224  by rw [mk_eq_mul_mk_one, (of Y).map_mul, mul_assoc, ←mk_eq_mul_mk_one, mk_self', mul_one]
id          └──────────────┘   └┘            └───────┘   └──────────────┘  └──────┘  └─────┘
src     └──┘└──────────────┘└┘ └┘ └─────────┘└───────┘└─┘└──────────────┘└┘└──────┘└┘└─────┘└─
typ     └──┘└──────────────┘└┘ └┘└─────────┘└───────┘└─┘└──────────────┘└┘└──────┘└┘└─────┘└─
doc     └──┘                └┘ └┘ └─────────┘         └─┘                └┘        └┘       └─
txt     └──┘                └┘    └─────────┘         └─┘                └┘        └┘       └─
par     └──┘                └┘    └─────────┘         └─┘                └┘        └┘       └─
pid       └┘                └┘    └─────────┘         └─┘                └┘        └┘       
st     └───────────────────┘└─────────────┘└──────────┘└─────────────────┘└────────┘└───────┘
225  
src  
typ  
doc  
txt  
par  
pid  
st   
226  @[simp, to_additive] lemma mk_mul_cancel_left (x : X) (y : Y) :
id                                                             
typ                                                            
doc    └──┘  └─────────┘
227    mk ((y : X) * x) y = of Y x :=
id     └┘             └┘  
src    └┘                 └┘
typ    └┘             └┘  
doc    └┘                   └┘
228  by rw [mul_comm, mk_mul_cancel_right]
id          └──────┘  └─────────────────┘
src     └──┘└──────┘└┘└─────────────────┘└─
typ     └──┘└──────┘└┘└─────────────────┘└─
doc     └──┘        └┘                   └─
txt     └──┘        └┘                   └─
par     └──┘        └┘                   └─
pid       └┘        └┘                   
st     └───────────┘└───────────────────┘
229  
src  
typ  
doc  
txt  
par  
pid  
st   
230  /-- Natural homomorphism sending `y ∈ Y`, `Y` a submonoid of a `comm_monoid` `X`, to the units of
231      the localization of `X` at `Y`. -/
232  def to_units (Y : submonoid X) : Y →* units (monoid_localization X Y) :=
id                     └───────┘      └┘ └───┘  └─────────────────┘  
src                    └───────┘        └┘ └───┘  └─────────────────┘
typ                    └───────┘      └┘ └───┘  └─────────────────┘  
doc                    └───────┘        └┘        └─────────────────┘
233  ⟨λ y, ⟨mk y 1, mk 1 y, by simp, by simp⟩, by simp; refl,
id         └┘     └┘   
src         └┘      └┘         └──┘     └──┘      └──┘  └──┘
typ        └┘     └┘        └──┘     └──┘      └──┘  └──┘
doc         └┘      └┘         └──┘     └──┘      └──┘  └──┘
txt                            └──┘     └──┘      └──┘  └──┘
par                            └──┘     └──┘      └──┘  └──┘
st                            └───┘    └───┘     └─────────┘
234   λ _ _, by ext; convert (of Y).map_mul _ _⟩
id                          └┘ 
src             └─┘  └──────┘ └┘ └───────────┘
typ           └─┘  └──────┘ └┘└───────────┘
doc             └─┘  └──────┘ └┘ └───────────┘
txt             └─┘  └──────┘    └───────────┘
par             └─┘  └──────┘    └───────────┘
pid                             └───────────┘
st             └──────────────────────────────┘
235  
236  @[simp] lemma to_units_mk (y) : (to_units Y y : monoid_localization X Y) = mk y 1 := rfl
id                                    └──────┘     └─────────────────┘     └┘       └─┘
src                                   └──────┘       └─────────────────┘       └┘        └─┘
typ                                   └──────┘     └─────────────────┘     └┘       └─┘
doc    └──┘                           └──────┘       └─────────────────┘        └┘
237  
238  @[simp] lemma mk_is_unit (y : Y) : is_unit (mk (y : X) (1 : Y)) :=
id                                     └─────┘  └┘            
src                                     └─────┘  └┘
typ                                    └─────┘  └┘            
doc    └──┘                             └─────┘  └┘
239  is_unit_unit $ to_units Y y
id   └──────────┘   └──────┘  
src  └──────────┘   └──────┘
typ  └──────────┘   └──────┘  
doc                 └──────┘
240  
241  @[simp] lemma mk_is_unit' (x) (hx : x ∈ Y) : is_unit (mk x (1 : Y)) :=
id                                             └─────┘  └┘       
src                                              └─────┘  └┘
typ                                            └─────┘  └┘       
doc    └──┘                                       └─────┘  └┘
242  is_unit_unit $ to_units Y ⟨x, hx⟩
id   └──────────┘   └──────┘     └┘
src  └──────────┘   └──────┘
typ  └──────────┘   └──────┘     └┘
doc                 └──────┘
243  
244  lemma to_units_inv (y) : mk 1 y = ↑(to_units Y y)⁻¹ := rfl
id                            └┘      └──────┘   └┘    └─┘
src                           └┘       └──────┘     └┘    └─┘
typ                           └┘      └──────┘   └┘    └─┘
doc                           └┘         └──────┘
245  
246  @[simp] lemma of_is_unit (y : Y) : is_unit (of Y y) :=
id                                     └─────┘  └┘  
src                                     └─────┘  └┘
typ                                    └─────┘  └┘  
doc    └──┘                             └─────┘  └┘
247  is_unit_unit $ to_units Y y
id   └──────────┘   └──────┘  
src  └──────────┘   └──────┘
typ  └──────────┘   └──────┘  
doc                 └──────┘
248  
249  @[simp] lemma of_is_unit' (x) (hx : x ∈ Y) : is_unit (of Y x) :=
id                                             └─────┘  └┘  
src                                              └─────┘  └┘
typ                                            └─────┘  └┘  
doc    └──┘                                       └─────┘  └┘
250  is_unit_unit $ to_units Y ⟨x, hx⟩
id   └──────────┘   └──────┘     └┘
src  └──────────┘   └──────┘
typ  └──────────┘   └──────┘     └┘
doc                 └──────┘
251  
252  lemma to_units_map_inv (g : monoid_localization X Y →* Z) (y) :
id                               └─────────────────┘   └┘ 
src                              └─────────────────┘     └┘
typ                              └─────────────────┘   └┘ 
doc                              └─────────────────┘     └┘
253    g ↑(to_units Y y)⁻¹ = ↑(units.map g (to_units Y y))⁻¹ :=
id       └──────┘   └┘   └───────┘   └──────┘    └┘
src       └──────┘     └┘   └───────┘    └──────┘      └┘
typ      └──────┘   └┘   └───────┘   └──────┘    └┘
doc        └──────┘                         └──────┘
254  by rw [←units.coe_map, (units.map g).map_inv]
id           └───────────┘   └───────┘ 
src     └───┘└───────────┘└┘ └───────┘ └──────────
typ     └───┘└───────────┘└┘ └───────┘└──────────
doc     └───┘             └┘           └──────────
txt     └───┘             └┘           └──────────
par     └───┘             └┘           └──────────
pid       └─┘             └┘           └────────┘
st     └─────────────────┘└────────────────────┘└┘
255  
src  
typ  
doc  
txt  
par  
pid  
st   
256  lemma mk_eq (x y) : mk x y = of Y x * ↑(to_units Y y)⁻¹ :=
id                       └┘    └┘     └──────┘   └┘
src                      └┘      └┘       └──────┘     └┘
typ                      └┘    └┘     └──────┘   └┘
doc                      └┘       └┘         └──────┘
257  by rw ←to_units_inv; simp only [of_eq_mk, mk_mul_mk, mul_one, one_mul]
id          └──────────┘             └──────┘  └───────┘  └─────┘  └─────┘
src     └──┘└──────────┘  └─────────┘└──────┘└┘└───────┘└┘└─────┘└┘└─────┘└─
typ     └──┘└──────────┘  └─────────┘└──────┘└┘└───────┘└┘└─────┘└┘└─────┘└─
doc     └──┘              └─────────┘        └┘         └┘       └┘       └─
txt     └──┘              └─────────┘        └┘         └┘       └┘       └─
par     └──┘              └─────────┘        └┘         └┘       └┘       └─
pid       └┘                  └──┘└┘        └┘         └┘       └┘       
st     └────────────────────────────────────────────────────────────────────
258  
src  
typ  
doc  
txt  
par  
pid  
st   
259  variables {f : X →* Z}
id                    └┘
src                   └┘
typ                   └┘
doc                   └┘
260  
261  lemma is_unit_of_of_comp {W : submonoid Z} (hf : ∀ y : Y, f y ∈ W) {y : Y} :
id                                 └───────┘                           
src                                └───────┘                       
typ                                └───────┘                           
doc                                └───────┘
262    is_unit (of W (f y)) :=
id     └─────┘  └┘    
src    └─────┘  └┘
typ    └─────┘  └┘    
doc    └─────┘  └┘
263  ⟨to_units W ⟨f y, hf y⟩, rfl⟩
id    └──────┘      └┘    └─┘
src   └──────┘                └─┘
typ   └──────┘      └┘    └─┘
doc   └──────┘
264  
265  variables {g : Y → units Z}
id                      └───┘
src                     └───┘
typ                     └───┘
266  
267  lemma units_restrict_mul (H : ∀ y : Y, f y = g y) {x y} : g (x * y) = g x * g y :=
id                                                                  
src                                                                         
typ                                                                 
268  by ext; rw [units.coe_mul, ←H _, ←H _, ←H _]; apply f.map_mul
id               └───────────┘             
src     └─┘  └──┘└───────────┘└─┘ └───┘ └───┘ └─┘  └────┘         
typ     └─┘  └──┘└───────────┘└─┘└───┘└───┘└─┘  └────┘         
doc     └─┘  └──┘             └─┘ └───┘ └───┘ └─┘  └────┘         
txt     └─┘  └──┘             └─┘ └───┘ └───┘ └─┘  └────┘         
par     └─┘  └──┘             └─┘ └───┘ └───┘ └─┘  └────┘         
pid            └┘             └─┘ └───┘ └───┘ └─┘                
st     └────────┘└───────────┘└────┘└────┘└────┘└─────────────────
269  
src  
typ  
doc  
txt  
par  
pid  
st   
270  variables (f)
271  
272  /-- Given a `comm_monoid` homomorphism `f : X → Z` mapping elements of a submonoid `Y` to
273      invertible elements of `Z`, the induced homomorphism from `Y` to the units of `Z`. -/
274  def units_restrict (H : ∀ y : Y, f y = g y) : Y →* units Z :=
id                                            └┘ └───┘ 
src                                                 └┘ └───┘
typ                                           └┘ └───┘ 
doc                                                  └┘
275  ⟨g, units.ext $ (H 1) ▸ f.map_one, λ _ _, units_restrict_mul H⟩
id      └───────┘         └──────┘       └────────────────┘ 
src      └───────┘           └──────┘         └────────────────┘
typ     └───────┘         └──────┘       └────────────────┘ 
doc                           └──────┘
276  
277  variables (g)
278  
279  /-- Given a `comm_monoid` homomorphism `f : X → Z` mapping elements of a submonoid `Y` to
280      invertible elements of `Z`, the homomorphism from `X × Y` to `Z` sending `(x, y)` to
281      `f(x) * f(y)⁻¹`; this induces a homomorphism from the localization of `X` at `Y`
282      (constructive version). -/
283  def aux (H : ∀ y : Y, f y = g y) : X × Y →* Z :=
id                                   └┘ 
src                                         └┘
typ                                  └┘ 
doc                                           └┘
284  (f.comp prod.monoid_hom.fst).mul $
id    └───┘ └─────────────────┘ └─┘
src    └───┘ └─────────────────┘ └─┘
typ   └───┘ └─────────────────┘ └─┘
doc    └───┘ └─────────────────┘ └─┘
285    (units.coe_hom Z).comp ((units_restrict f H).comp prod.monoid_hom.snd).inv
id      └───────────┘  └──┘    └────────────┘   └──┘  └─────────────────┘ └─┘
src     └───────────┘   └──┘    └────────────┘     └──┘  └─────────────────┘ └─┘
typ     └───────────┘  └──┘    └────────────┘   └──┘  └─────────────────┘ └─┘
doc     └───────────┘   └──┘    └────────────┘     └──┘  └─────────────────┘ └─┘
286  
287  variables {g}
288  
289  /-- Given a `comm_monoid` homomorphism `f : X → Z` mapping elements of a submonoid `Y` to
290      invertible elements of `Z`, the homomorphism from `X × Y` to `Z` sending `(x, y)` to
291      `f(x) * f(y)⁻¹` is constant on the equivalence classes of the localization of `X` at `Y`. -/
292  lemma r_le_ker_aux (H : ∀ y : Y, f y = g y) :
id                                       
src                                       
typ                                      
293    Y.r ≤ con.ker (aux f g H) :=
id     └┘  └─────┘  └─┘   
src     └┘  └─────┘  └─┘
typ    └┘  └─────┘  └─┘   
doc     └┘   └─────┘  └─┘
294  con.Inf_le _ _ (λ y, show f (1 : Y) * ↑(g 1)⁻¹ = f y * ↑(g y)⁻¹, by
id   └────────┘                            └┘        └┘
src  └────────┘                                └┘            └┘
typ  └────────┘                            └┘        └┘
doc  └────────┘
st                                                                      
295    rw [H 1, H y]; simp [units.mul_inv])
id                       └───────────┘
src    └──┘ └──┘    └────┘└───────────┘
typ    └──┘└──┘  └────┘└───────────┘
doc    └──┘ └──┘    └────┘             
txt    └──┘ └──┘    └────┘             
par    └──┘ └──┘    └────┘             
pid      └┘ └──┘                     
st   ───────┘└────┘└────────────────────┘
296  
297  /-- Given a `comm_monoid` homomorphism `f : X → Z` mapping elements of a submonoid `Y` to
298      invertible elements of `Z`, the homomorphism from the localization of `X` at `Y` sending
299      `⟦(x, y)⟧` to `f(x) * f(y)⁻¹`. -/
300  def lift' (g : Y → units Z) (H : ∀ y : Y, f y = g y) : monoid_localization X Y →* Z :=
id                     └───┘                        └─────────────────┘   └┘ 
src                     └───┘                              └─────────────────┘     └┘
typ                    └───┘                        └─────────────────┘   └┘ 
doc                                                         └─────────────────┘     └┘
301  Y.r.lift (aux f g H) $ r_le_ker_aux f H
id   └┘└───┘  └─┘       └──────────┘  
src   └┘└───┘  └─┘          └──────────┘
typ  └┘└───┘  └─┘       └──────────┘  
doc   └┘└───┘  └─┘          └──────────┘
302  
303  /-- Given a `comm_monoid` homomorphism `f : X → Z` mapping elements of a submonoid `Y` to
304      invertible elements of `Z`, the homomorphism from the localization of `X` at `Y` sending
305      `⟦(x, y)⟧` to `f(x) * f(y)⁻¹`, where `f(y)⁻¹` is chosen nonconstructively. -/
306  noncomputable def lift (H : ∀ y : Y, is_unit (f y)) : monoid_localization X Y →* Z :=
id                                       └─────┘        └─────────────────┘   └┘ 
src                                       └─────┘          └─────────────────┘     └┘
typ                                      └─────┘        └─────────────────┘   └┘ 
doc                                       └─────┘          └─────────────────┘     └┘
307  lift' f _ $ λ _, classical.some_spec $ H _
id   └───┘          └─────────────────┘   
src  └───┘            └─────────────────┘
typ  └───┘          └─────────────────┘   
doc  └───┘
308  
309  variables {f}
310  
311  @[simp] lemma lift'_mk (H : ∀ y : Y, f y = g y) (x y) :
id                                           
src                                           
typ                                          
doc    └──┘
312    lift' f _ H (mk x y) = f x * ↑(g y)⁻¹ := rfl
id     └───┘      └┘           └┘    └─┘
src    └───┘        └┘                 └┘    └─┘
typ    └───┘      └┘           └┘    └─┘
doc    └───┘        └┘
313  
314  @[simp] lemma lift_mk (H : ∀ y : Y, is_unit (f y)) (x y) :
id                                      └─────┘   
src                                      └─────┘
typ                                     └─────┘   
doc    └──┘                              └─────┘
315    lift f H (mk x y) = f x * ↑(classical.some (H y))⁻¹ := rfl
id     └──┘    └┘         └────────────┘     └┘    └─┘
src    └──┘      └┘             └────────────┘       └┘    └─┘
typ    └──┘    └┘         └────────────┘     └┘    └─┘
doc    └──┘      └┘
316  
317  @[simp] lemma lift'_of (H : ∀ y : Y, f y = g y) (x : X) :
id                                                  
src                                           
typ                                                 
doc    └──┘
318    lift' f _ H (of Y x) = f x :=
id     └───┘      └┘      
src    └───┘        └┘      
typ    └───┘      └┘      
doc    └───┘        └┘
319  show f x * ↑(g 1)⁻¹ = _, by
id               └┘ 
src                 └┘ 
typ              └┘ 
st                              
320    rw [inv_eq_one.2 (show g 1 = 1, from units.ext $ (H 1) ▸ f.map_one), units.coe_one, mul_one]
id         └────────┘                     └───────┘         └───────┘   └───────────┘  └─────┘
src    └──┘└────────┘└─┘      └─┘└───────┘└───────┘   └──┘└───────┘└─┘└───────────┘└┘└─────┘└─
typ    └──┘└────────┘└─┘     └─┘└───────┘└───────┘  └──┘└───────┘└─┘└───────────┘└┘└─────┘└─
doc    └──┘          └─┘      └─┘ └───────┘            └──┘ └───────┘└─┘             └┘       └─
txt    └──┘          └─┘      └─┘ └───────┘            └──┘          └─┘             └┘       └─
par    └──┘          └─┘      └─┘ └───────┘            └──┘          └─┘             └┘       └─
pid      └┘          └─┘      └─┘ └───────┘            └──┘          └─┘             └┘       
st   ────────────────────────────────────────────────────────────────────┘└─────────────┘└───────┘
321  
src  
typ  
doc  
txt  
par  
pid  
st   
322  @[simp] lemma lift_of (H : ∀ y : Y, is_unit (f y)) (x : X) :
id                                      └─────┘           
src                                      └─────┘
typ                                     └─────┘           
doc    └──┘                              └─────┘
323    lift f H (of Y x) = f x := lift'_of _ _
id     └──┘    └┘          └──────┘
src    └──┘      └┘              └──────┘
typ    └──┘    └┘          └──────┘
doc    └──┘      └┘
324  
325  lemma lift'_eq_iff (H : ∀ y : Y, f y = g y) {x y : X × Y} :
id                                                  
src                                                      
typ                                                 
326    lift' f g H (mk x.1 x.2) = lift' f g H (mk y.1 y.2) ↔ f (y.2 * x.1) = f (y.1 * x.2) :=
id     └───┘     └┘       └───┘     └┘                     
src    └───┘        └┘         └───┘        └┘                             
typ    └───┘     └┘       └───┘     └┘                     
doc    └───┘        └┘            └───┘        └┘
327  by rw [lift'_mk, lift'_mk, units.eq_mul_inv_iff_mul_eq, mul_comm, ←mul_assoc,
id          └──────┘  └──────┘  └─────────────────────────┘  └──────┘   └───────┘
src     └──┘└──────┘└┘└──────┘└┘└─────────────────────────┘└┘└──────┘└─┘└───────┘└─
typ     └──┘└──────┘└┘└──────┘└┘└─────────────────────────┘└┘└──────┘└─┘└───────┘└─
doc     └──┘        └┘        └┘                           └┘        └─┘         └─
txt     └──┘        └┘        └┘                           └┘        └─┘         └─
par     └──┘        └┘        └┘                           └┘        └─┘         └─
pid       └┘        └┘        └┘                           └┘        └─┘         └─
st     └───────────┘└────────┘└───────────────────────────┘└────────┘└──────────┘└─
328         units.mul_inv_eq_iff_eq_mul, ←H _, ←H _, ←f.map_mul, ←f.map_mul]
id          └─────────────────────────┘        
src  ──────┘└─────────────────────────┘└─┘ └───┘ └───┘         └─┘         └─
typ  ──────┘└─────────────────────────┘└─┘└───┘└───┘└───────┘└─┘└───────┘└─
doc  ──────┘                           └─┘ └───┘ └───┘         └─┘         └─
txt  ──────┘                           └─┘ └───┘ └───┘         └─┘         └─
par  ──────┘                           └─┘ └───┘ └───┘         └─┘         └─
pid  ──────┘                           └─┘ └───┘ └───┘         └─┘         
st   ─────────────────────────────────┘└────┘└────┘└──────────┘└──────────┘
329  
src  
typ  
doc  
txt  
par  
pid  
st   
330  lemma lift_eq_iff (H : ∀ y : Y, is_unit (f y)) {x y : X × Y} :
id                                  └─────┘               
src                                  └─────┘                 
typ                                 └─────┘               
doc                                  └─────┘
331    lift f H (mk x.1 x.2) = lift f H (mk y.1 y.2) ↔ f (y.2 * x.1) = f (y.1 * x.2) :=
id     └──┘    └┘       └──┘    └┘                     
src    └──┘      └┘         └──┘      └┘                             
typ    └──┘    └┘       └──┘    └┘                     
doc    └──┘      └┘            └──┘      └┘
332  lift'_eq_iff _
id   └──────────┘
src  └──────────┘
typ  └──────────┘
333  
334  lemma mk_eq_iff_of_eq {x y : X × Y} :
id                                  
src                                 
typ                                 
335    mk x.1 x.2 = mk y.1 y.2 ↔ of Y (y.2 * x.1) = of Y (y.1 * x.2) :=
id     └┘      └┘      └┘          └┘      
src    └┘        └┘        └┘             └┘         
typ    └┘      └┘      └┘          └┘      
doc    └┘           └┘           └┘                 └┘
336  by rw [mk_eq, mk_eq, ←lift'_mk, ←lift'_mk];
id          └───┘  └───┘   └──────┘   └──────┘
src     └──┘└───┘└┘└───┘└─┘└──────┘└─┘└──────┘
typ     └──┘└───┘└┘└───┘└─┘└──────┘└─┘└──────┘
doc     └──┘     └┘     └─┘        └─┘        
txt     └──┘     └┘     └─┘        └─┘        
par     └──┘     └┘     └─┘        └─┘        
pid       └┘     └┘     └─┘        └─┘        
st     └────────┘└─────┘└─────────┘└─────────┘└─
337    exact lift'_eq_iff (λ (w : Y), rfl)
id           └──────────┘            └─┘
src    └────┘└──────────┘  └────┘ └─┘└─┘└─
typ    └────┘└──────────┘  └────┘└─┘└─┘└─
doc    └────┘              └────┘ └─┘   └─
txt    └────┘              └────┘ └─┘   └─
par    └────┘              └────┘ └─┘   └─
pid                       └────┘ └─┘   
st   ──────────────────────────────────────
338  
src  
typ  
doc  
txt  
par  
pid  
st   
339  lemma lift'_comp_of (H : ∀ y : Y, f y = g y) :
id                                        
src                                        
typ                                       
340    (lift' f _ H).comp (of Y) = f :=
id      └───┘     └──┘   └┘    
src     └───┘       └──┘   └┘    
typ     └───┘     └──┘   └┘    
doc     └───┘       └──┘   └┘
341  by ext; exact lift'_of H _
id                 └──────┘ 
src     └─┘  └────┘└──────┘ └──
typ     └─┘  └────┘└──────┘└──
doc     └─┘  └────┘         └──
txt     └─┘  └────┘         └──
par     └─┘  └────┘         └──
pid                        └┘
st     └────────────────────────
342  
src  
typ  
doc  
txt  
par  
pid  
st   
343  @[simp] lemma lift_comp_of (H : ∀ y : Y, is_unit (f y)) :
id                                           └─────┘   
src                                           └─────┘
typ                                          └─────┘   
doc    └──┘                                   └─────┘
344    (lift f H).comp (of Y) = f := lift'_comp_of _
id      └──┘   └──┘   └┘        └───────────┘
src     └──┘     └──┘   └┘          └───────────┘
typ     └──┘   └──┘   └┘        └───────────┘
doc     └──┘     └──┘   └┘
345  
346  @[simp] lemma lift'_apply_of (f' : monoid_localization X Y →* Z)
id                                      └─────────────────┘   └┘ 
src                                     └─────────────────┘     └┘
typ                                     └─────────────────┘   └┘ 
doc    └──┘                             └─────────────────┘     └┘
347    (H : ∀ y : Y, f'.comp (of Y) y = g y) : lift' (f'.comp (of Y)) _ H = f' :=
id                  └┘└───┘  └┘          └───┘  └┘└───┘  └┘        └┘
src                    └───┘  └┘              └───┘    └───┘  └┘         
typ                 └┘└───┘  └┘          └───┘  └┘└───┘  └┘        └┘
doc                    └───┘  └┘               └───┘    └───┘  └┘
348  begin
st   └─────
349    ext x,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
350    apply induction_on x,
id           └──────────┘ 
src    └────┘└──────────┘
typ    └────┘└──────────┘
doc    └────┘            
txt    └────┘            
par    └────┘            
pid                     
st   ─────────────────────┘└─
351    intros,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
st   ───────┘└─
352    rw [lift'_mk, ←units.mul_right_inj (g y.2), mul_assoc, units.inv_mul, ←H y.2,
id         └──────┘   └─────────────────┘        └───────┘  └───────────┘    
src    └──┘└──────┘└─┘└─────────────────┘   └───┘└───────┘└┘└───────────┘└─┘  └───
typ    └──┘└──────┘└─┘└─────────────────┘ └───┘└───────┘└┘└───────────┘└─┘└───
doc    └──┘        └─┘                      └───┘         └┘             └─┘  └───
txt    └──┘        └─┘                      └───┘         └┘             └─┘  └───
par    └──┘        └─┘                      └───┘         └┘             └─┘  └───
pid      └┘        └─┘                      └───┘         └┘             └─┘  └───
st   ─────────────┘└────────────────────────────┘└─────────┘└─────────────┘└────┘└───
353        mul_one, mk_eq_mul_mk_one],
id         └─────┘  └──────────────┘
src  ─────┘└─────┘└┘└──────────────┘
typ  ─────┘└─────┘└┘└──────────────┘
doc  ─────┘       └┘                
txt  ─────┘       └┘                
par  ─────┘       └┘                
pid  ─────┘       └┘                
st   ────────────┘└────────────────┘└──
354    show f' _ = f' (mk _ _ * _) * f' (mk _ _),
id                                 └┘  └┘
src    └───┘  └─┘     └───┘└──┘    └┘└───┘
typ    └───┘  └─┘     └───┘└──┘ └┘ └┘└───┘
doc    └───┘  └─┘      └───┘ └──┘    └┘└───┘
txt    └───┘  └─┘      └───┘ └──┘      └───┘
par    └───┘  └─┘      └───┘ └──┘      └───┘
pid    └───┘  └─┘      └───┘ └──┘      └───┘
st   ──────────────────────────────────────────┘└─
355    rw [←f'.map_mul, mk_mul_mk, mk_mul_mk],
id                      └───────┘  └───────┘
src    └───┘          └┘└───────┘└┘└───────┘
typ    └───┘└────────┘└┘└───────┘└┘└───────┘
doc    └───┘          └┘         └┘         
txt    └───┘          └┘         └┘         
par    └───┘          └┘         └┘         
pid      └─┘          └┘         └┘         
st   ────────────────┘└─────────┘└─────────┘└──
356    simp only [mul_one, mk_mul_cancel_right, one_mul],
id                └─────┘  └─────────────────┘  └─────┘
src    └─────────┘└─────┘└┘└─────────────────┘└┘└─────┘
typ    └─────────┘└─────┘└┘└─────────────────┘└┘└─────┘
doc    └─────────┘       └┘                   └┘       
txt    └─────────┘       └┘                   └┘       
par    └─────────┘       └┘                   └┘       
pid        └──┘└┘       └┘                   └┘       
st   ──────────────────────────────────────────────────┘└─
357  end
st   ──┘
358  
359  @[simp] lemma lift_apply_of (g : monoid_localization X Y →* Z) :
id                                    └─────────────────┘   └┘ 
src                                   └─────────────────┘     └┘
typ                                   └─────────────────┘   └┘ 
doc    └──┘                           └─────────────────┘     └┘
360    lift (g.comp $ of Y) (λ y, is_unit_unit $ units.map g $ to_units Y y) = g :=
id     └──┘  └───┘   └┘        └──────────┘   └───────┘    └──────┘     
src    └──┘   └───┘   └┘          └──────────┘   └───────┘     └──────┘      
typ    └──┘  └───┘   └┘        └──────────┘   └───────┘    └──────┘     
doc    └──┘   └───┘   └┘                                       └──────┘
361  lift'_apply_of _ _
id   └────────────┘
src  └────────────┘
typ  └────────────┘
362  
363  lemma  funext (f g : monoid_localization X Y →* Z)
id                        └─────────────────┘   └┘ 
src                       └─────────────────┘     └┘
typ                       └─────────────────┘   └┘ 
doc                       └─────────────────┘     └┘
364    (h : ∀ a, f.comp (of Y) a = g.comp (of Y) a) : f = g :=
id              └───┘  └┘     └───┘  └┘         
src               └───┘  └┘        └───┘  └┘           
typ             └───┘  └┘     └───┘  └┘         
doc               └───┘  └┘         └───┘  └┘
365  begin
st   └─────
366    rw [←lift_apply_of f, ←lift_apply_of g],
id          └───────────┘    └───────────┘ 
src    └───┘└───────────┘ └─┘└───────────┘ 
typ    └───┘└───────────┘└─┘└───────────┘
doc    └───┘              └─┘              
txt    └───┘              └─┘              
par    └───┘              └─┘              
pid      └─┘              └─┘              
st   ─────────────────────┘└────────────────┘└──
367    congr' 1,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid          
st   ─────────┘└─
368    ext,
src    └─┘
typ    └─┘
doc    └─┘
txt    └─┘
par    └─┘
st   ────┘└─
369    convert h x,
id              
src    └──────┘ 
typ    └──────┘
doc    └──────┘ 
txt    └──────┘ 
par    └──────┘ 
pid            
st   ────────────┘└─
370  end
st   ──┘
371  
372  variables {W : submonoid Z} (f)
id                  └───────┘
src                 └───────┘
typ                 └───────┘
doc                 └───────┘
373  
374  /-- Given a `comm_monoid` homomorphism `f : X → Z` where for submonoids `Y ⊆ X, W ⊆ Z` we have
375      `f(Y) ⊆ W`, the monoid homomorphism from the localization of `X` at `Y` to the localization of
376      `Z` at `W` induced by the natural map from `Z` to the localization of `Z` at
377      `W` composed with `f`. -/
378  def map (hf : ∀ y : Y, f y ∈ W) : monoid_localization X Y →* monoid_localization Z W :=
id                                └─────────────────┘   └┘ └─────────────────┘  
src                                   └─────────────────┘     └┘ └─────────────────┘
typ                               └─────────────────┘   └┘ └─────────────────┘  
doc                                    └─────────────────┘     └┘ └─────────────────┘
379  lift' ((of W).comp f) ((to_units W).comp $ (f.comp Y.subtype).subtype_mk W hf) $ λ y, rfl
id   └───┘   └┘  └──┘      └──────┘  └──┘     └───┘ └──────┘ └────────┘   └┘        └─┘
src  └───┘   └┘   └──┘       └──────┘   └──┘      └───┘  └──────┘ └────────┘               └─┘
typ  └───┘   └┘  └──┘      └──────┘  └──┘     └───┘ └──────┘ └────────┘   └┘        └─┘
doc  └───┘   └┘   └──┘       └──────┘   └──┘      └───┘  └──────┘ └────────┘
380  
381  variables {f}
382  
383  lemma map_eq (hf : ∀ y : Y, f y ∈ W) :
id                                 
src                                  
typ                                
384    map f hf = lift ((of W).comp f) (λ y, ⟨to_units W ⟨f y, hf y⟩, rfl⟩) :=
id     └─┘  └┘  └──┘   └┘  └──┘          └──────┘      └┘    └─┘
src    └─┘       └──┘   └┘   └──┘            └──────┘                └─┘
typ    └─┘  └┘  └──┘   └┘  └──┘          └──────┘      └┘    └─┘
doc    └─┘        └──┘   └┘   └──┘            └──────┘
385  by rw map; congr; ext; erw ←classical.some_spec (is_unit_of_of_comp hf); refl
id         └─┘                   └─────────────────┘  └────────────────┘ └┘
src     └─┘└─┘  └───┘  └─┘  └───┘└─────────────────┘ └────────────────┘    └────
typ     └─┘└─┘  └───┘  └─┘  └───┘└─────────────────┘ └────────────────┘└┘  └────
doc     └─┘└─┘         └─┘  └───┘                                          └────
txt     └─┘     └───┘  └─┘  └───┘                                          └────
par     └─┘     └───┘  └─┘  └───┘                                          └────
pid                           └┘                                              
st     └───────────────────────────────────────────────────────────────────────────
386  
src  
typ  
doc  
txt  
par  
pid  
st   
387  @[simp] lemma map_of (hf : ∀ y : Y, f y ∈ W) (x) :
id                                         
src                                          
typ                                        
doc    └──┘
388    map f hf (of Y x) = of W (f x) := lift'_of _ _
id     └─┘  └┘  └┘     └┘         └──────┘
src    └─┘       └┘       └┘            └──────┘
typ    └─┘  └┘  └┘     └┘         └──────┘
doc    └─┘       └┘        └┘
389  
390  @[simp] lemma map_comp_of (hf : ∀ y : Y, f y ∈ W) :
id                                              
src                                               
typ                                             
doc    └──┘
391    (map f hf).comp (of Y) = (of W).comp f := lift'_comp_of _
id      └─┘  └┘ └──┘   └┘     └┘  └──┘      └───────────┘
src     └─┘      └──┘   └┘      └┘   └──┘       └───────────┘
typ     └─┘  └┘ └──┘   └┘     └┘  └──┘      └───────────┘
doc     └─┘      └──┘   └┘       └┘   └──┘
392  
393  lemma map_mk (hf : ∀ y : Y, f y ∈ W) (x y) :
id                                 
src                                  
typ                                
394    map f hf (mk x y) = mk (f x) ⟨f y, hf y⟩ :=
id     └─┘  └┘  └┘     └┘         └┘ 
src    └─┘       └┘       └┘
typ    └─┘  └┘  └┘     └┘         └┘ 
doc    └─┘       └┘        └┘
395  (lift'_mk _ _ _).trans (mk_eq _ _).symm
id    └──────┘       └───┘   └───┘     └──┘
src   └──────┘       └───┘   └───┘     └──┘
typ   └──────┘       └───┘   └───┘     └──┘
396  
397  @[simp] lemma map_id (x : monoid_localization X Y) :
id                             └─────────────────┘  
src                            └─────────────────┘
typ                            └─────────────────┘  
doc    └──┘                    └─────────────────┘
398    map (monoid_hom.id X) (λ (y : Y), y.2) x = x :=
id     └─┘  └───────────┘                   
src    └─┘  └───────────┘                      
typ    └─┘  └───────────┘                   
doc    └─┘  └───────────┘
399  induction_on x $ λ ⟨w, z⟩, by rw map_mk; exact congr_arg _ (subtype.eq' rfl)
id   └──────────┘                   └────┘        └───────┘    └─────────┘ └─┘
src  └──────────┘                  └─┘└────┘  └────┘└───────┘└─┘ └─────────┘└─┘└─
typ  └──────────┘                └─┘└────┘  └────┘└───────┘└─┘ └─────────┘└─┘└─
doc                                └─┘        └────┘         └─┘               └─
txt                                └─┘        └────┘         └─┘               └─
par                                └─┘        └────┘         └─┘               └─
pid                                                        └─┘               
st                                └───────────────────────────────────────────────
400  
src  
typ  
doc  
txt  
par  
pid  
st   
401  lemma map_comp_map {A} [comm_monoid A] {V} {g : Z →* A}
id                           └─────────┘             └┘ 
src                          └─────────┘               └┘
typ                          └─────────┘             └┘ 
doc                                                    └┘
402    (hf : ∀ y : Y, f y ∈ W) (hg : ∀ w : W, g w ∈ V) :
id                                         
src                                              
typ                                        
403    (map g hg).comp (map f hf) = map (g.comp f) (λ y, hg ⟨f y, hf y⟩) :=
id      └─┘  └┘ └──┘   └─┘  └┘   └─┘  └───┘        └┘     └┘ 
src     └─┘      └──┘   └─┘        └─┘   └───┘
typ     └─┘  └┘ └──┘   └─┘  └┘   └─┘  └───┘        └┘     └┘ 
doc     └─┘      └──┘   └─┘         └─┘   └───┘
404  funext _ _ $ λ x, by simp only [map_of, monoid_hom.comp_apply]
id   └────┘                         └────┘  └───────────────────┘
src  └────┘               └─────────┘└────┘└┘└───────────────────┘└─
typ  └────┘              └─────────┘└────┘└┘└───────────────────┘└─
doc                       └─────────┘      └┘                     └─
txt                       └─────────┘      └┘                     └─
par                       └─────────┘      └┘                     └─
pid                           └──┘└┘      └┘                     
st                       └──────────────────────────────────────────
405  
src  
typ  
doc  
txt  
par  
pid  
st   
406  lemma map_map {A} [comm_monoid A] {V} {g : Z →* A}
id                      └─────────┘             └┘ 
src                     └─────────┘               └┘
typ                     └─────────┘             └┘ 
doc                                               └┘
407    (hf : ∀ y : Y, f y ∈ W) (hg : ∀ w : W, g w ∈ V) (x) :
id                                         
src                                              
typ                                        
408    map g hg (map f hf x) = map (g.comp f) (λ y : Y, hg ⟨f y, hf y⟩) x :=
id     └─┘  └┘  └─┘  └┘    └─┘  └───┘            └┘     └┘    
src    └─┘       └─┘          └─┘   └───┘
typ    └─┘  └┘  └─┘  └┘    └─┘  └───┘            └┘     └┘    
doc    └─┘       └─┘           └─┘   └───┘
409  by rw ←map_comp_map hf hg; refl
id          └──────────┘ └┘ └┘
src     └──┘└──────────┘      └────
typ     └──┘└──────────┘└┘└┘  └────
doc     └──┘                  └────
txt     └──┘                  └────
par     └──┘                  └────
pid       └┘                      
st     └─────────────────────────────
410  
src  
typ  
doc  
txt  
par  
pid  
st   
411  lemma map_ext (g : X →* Z) (hf : ∀ y : Y, f y ∈ W) (hg : ∀ y : Y, g y ∈ W)
id                       └┘                                       
src                       └┘                                              
typ                      └┘                                       
doc                       └┘
412    (h : f = g) (x) : map f hf x = map g hg x :=
id                    └─┘  └┘   └─┘  └┘ 
src                     └─┘         └─┘
typ                   └─┘  └┘   └─┘  └┘ 
doc                      └─┘          └─┘
413  induction_on x $ λ _, by {rw [map_mk, map_mk], congr; rw h; refl}
id   └──────────┘                └────┘  └────┘             
src  └──────────┘              └──┘└────┘└┘└────┘  └───┘  └─┘   └──┘
typ  └──────────┘            └──┘└────┘└┘└────┘  └───┘  └─┘  └──┘
doc                            └──┘      └┘               └─┘   └──┘
txt                            └──┘      └┘        └───┘  └─┘   └──┘
par                            └──┘      └┘        └───┘  └─┘   └──┘
pid                              └┘      └┘                 
st                           └──────────┘└──────┘└───────────┘└────┘└┘
414  
415  end monoid_localization